T:Type, P:(T), as:T List, d:T.
(first a  as s.t. P(a) else d  as)  (first a  as s.t. P(a) else d) = d 

latex

Definitions	x:A. B(x), b, t  T, A, b, Prop, , x(s), P  Q, P & Q, P  Q, Unit, (x  l), {T}, P  Q, True, first x  as s.t. P(x) else d, P  Q, x. t(x)
Lemmas	find wf, cons member, l member wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, assert wf